Nuprl Lemma : ss-atoms-distinct 0,22
es:ES, i:Id, L:IdLnk List, T:(IdType).
es-secret-server{table:ut2, encrypt:ut2, decrypt:ut2}
es-secret-server(es; T; L; i)
 e1@i.
 e2@i.
 n:||"table" when e1|| , m:||"table" when e2|| .
 st-atom("table" when e1;n) = st-atom("table" when e2;m)  Atom1  n = m   
latex

Definitionsatoms-distinct(tab), True, true, e@i. P(e), b, t  T, Id, if b t else f fi, x:A. B(x), T, i  j < k, "$x", {i..j}, Prop, P  Q, P & Q, es-secret-server, @i only events in L change   x : T, A & B, , False, let x = a in b(x), AB, A
Lemmases-loc wf, es-loc-init, Id wf, int seg wf, es-init wf, secret-table wf, es-when wf, es-vartype wf, squash wf, true wf, es-E wf, event system wf, es-first-init, le wf, IdLnk wf, es-secret-server wf, st-length wf, nat wf, ss-atom-constant, es-first-unique, ss-table-length, st-atom wf

origin